r:Rng, a:|r|. (0 * a) = 0  |r| & (a * 0) = 0  |r| 

latex

Up	rings 1
Definitions of Statement	Rng
Definitions	t  T, x:A. B(x), P  Q, P  Q, P  Q, x f y, P & Q, Rng
Lemmas	rng wf, rng car wf, rng zero wf, rng plus zero, rng times wf, rng times over plus, rng plus cancel l